COMMENT ⊗   VALID 00005 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	subst[f83,jmc]		Proofs about subst
C00005 00003	(decl subst (type: |groundgroundground→ground|) (syntype: constant))
C00011 00004	file read in
C00016 00005	60. 
C00017 ENDMK
C⊗;
subst[f83,jmc]		Proofs about subst
(decl subst (type: |ground⊗ground⊗ground→ground|) (syntype: constant))
;Z1 is unknown.
;Z2 is unknown.
;the symbol Z2 is given the same declaration as Z
;the symbol Z1 is given the same declaration as Z
;define: could not deduce the validity of this definition:
∃SUBST.(∀X Y Z Z1 Z2.ATOM Z⊃
                     (IF Y=Z THEN SUBST(X,Y,Y)=X ELSE SUBST(X,Y,Z)=Z)∧
                     SUBST(X,Y,Z1.Z2)=SUBST(X,Y,Z1).SUBST(X,Y,Z2))
;did not re-write to true.
60. 
(define subst |∀x y z z1 z2.atom z ⊃ (subst(x,y,z) = if (y=z) then x else z) ∧
subst(x,y,z1.z2) = subst(x,y,z1).subst(x,y,z2)| (use sexpinductiondef))
;Z1 is unknown.
;Z2 is unknown.
;the symbol Z2 is given the same declaration as Z
;the symbol Z1 is given the same declaration as Z
;define: could not deduce the validity of this definition:
∃SUBST.(∀X Y Z Z1 Z2.ATOM Z⊃
                     (IF Z=Y THEN SUBST(X,Y,Y)=X ELSE SUBST(X,Y,Z)=Z)∧
                     SUBST(X,Y,Z1.Z2)=SUBST(X,Y,Z1).SUBST(X,Y,Z2))
;did not re-write to true.
60. 

(define subst |∀x y z z1 z2.atom z ⊃ (if z=y then subst(x,y,z) = x
else subst(x,y,z) = z) ∧
subst(x,y,z1.z2) = subst(x,y,z1).subst(x,y,z2)| (use sexpinductiondef))
;Z1 is unknown.
;Z2 is unknown.
;the symbol Z2 is given the same declaration as Z
;the symbol Z1 is given the same declaration as Z
;define: could not deduce the validity of this definition:
∃SUBST.(∀X Y Z Z1 Z2.ATOM Z⊃
                     (IF Z=Y THEN SUBST(X,Y,Y)=X ELSE SUBST(X,Y,Z)=Z)∧
                     SUBST(X,Y,Z1.Z2)=SUBST(X,Y,Z1).SUBST(X,Y,Z2))
;did not re-write to true.
60. 
(decl subst (type: |ground⊗ground⊗ground→ground|) (syntype: constant))
(defax subst |∀x y z z1 z2.(atom z ⊃ subst(x,y,z) = if z = y then x else z)
∧ subst(x,y,z1.z2) = subst(x,y,z1).subst(x,y,z2)|)
(setq rewritemessages t)
(ue (phi |λz.subst(x,y,subst(x,y,z)) = subst(subst(x,y,x),y,z)|)
sexpinduction (open subst))
(∀X1.ATOM X1⊃
     (IF X1=Y THEN SUBST(X,X1,X)=SUBST(SUBST(X,X1,X),X1,X1)
         ELSE X1=SUBST(SUBST(X,Y,X),Y,X1)))∧
(∀X2 Y1.SUBST(X,Y,SUBST(X,Y,X2))=SUBST(SUBST(X,Y,X),Y,X2)∧
        SUBST(X,Y,SUBST(X,Y,Y1))=SUBST(SUBST(X,Y,X),Y,Y1)⊃
        SUBST(X,Y,SUBST(X,Y,X2).SUBST(X,Y,Y1))=SUBST(SUBST(X,Y,X),Y,X2.Y1))⊃
(∀X3.SUBST(X,Y,SUBST(X,Y,X3))=SUBST(SUBST(X,Y,X),Y,X3))

62. 
60. (DEFAX SUBST
      |∀X Y Z Z1 Z2.(ATOM Z⊃SUBST(X,Y,Z)=(IF Z=Y THEN X ELSE Z))∧
                    SUBST(X,Y,Z1.Z2)=SUBST(X,Y,Z1).SUBST(X,Y,Z2)|)

62. 
(show 60)
;the term SUBST(X,Y,X4) is replaced by:
;IF X4=Y THEN X ELSE X4
;the term SUBST(X,Y,IF X4=Y THEN X ELSE X4) is replaced by:
;IF X4=Y THEN SUBST(X,Y,X) ELSE SUBST(X,Y,X4)
;the term Y is replaced by:
;X4
;the term SUBST(X,Y,X4) is replaced by:
;IF X4=Y THEN X ELSE X4
;the term X4=Y is replaced by:
;FALSE
;the term IF FALSE THEN X ELSE X4 is replaced by:
;X4
;the term (IF X4=Y THEN SUBST(X,X4,X) ELSE X4)=SUBST(SUBST(X,Y,X),Y,X4) 
is replaced by:
;IF X4=Y THEN SUBST(X,X4,X)=SUBST(SUBST(X,Y,X),Y,X4) ELSE X4=SUBST(SUBST(X,Y,X),Y,X4)
;the term Y is replaced by:
;X4
;the term Y is replaced by:
;X4
;the term SUBST(X,Y,X5.Y2) is replaced by:
;SUBST(X,Y,X5).SUBST(X,Y,Y2)
(∀X4.ATOM X4⊃
     (IF X4=Y THEN SUBST(X,X4,X)=SUBST(SUBST(X,X4,X),X4,X4)
         ELSE X4=SUBST(SUBST(X,Y,X),Y,X4)))∧
(∀X5 Y2.SUBST(X,Y,SUBST(X,Y,X5))=SUBST(SUBST(X,Y,X),Y,X5)∧
        SUBST(X,Y,SUBST(X,Y,Y2))=SUBST(SUBST(X,Y,X),Y,Y2)⊃
        SUBST(X,Y,SUBST(X,Y,X5).SUBST(X,Y,Y2))=SUBST(SUBST(X,Y,X),Y,X5.Y2))⊃
(∀X6.SUBST(X,Y,SUBST(X,Y,X6))=SUBST(SUBST(X,Y,X),Y,X6))

63. 

(decl subst1 (type: |ground⊗ground⊗ground→ground|) (syntype: constant))
(defax subst1 |∀x y z z1 z2.(atom z ⊃ (z = y ⊃ subst1(x,y,z) = x) ∧
(¬(z = y) ⊃ subst1(x,y,z) = z))
∧ subst1(x,y,z1.z2) = subst1(x,y,z1).subst1(x,y,z2)|)
(ue (phi |λz.subst1(x,y,subst1(x,y,z)) = subst1(subst1(x,y,x),y,z)|)
sexpinduction (open subst1) (der))
;the term SUBST1(X,Y,X8.Y3) is replaced by:
;SUBST1(X,Y,X8).SUBST1(X,Y,Y3)
(∀X7.ATOM X7⊃SUBST1(X,Y,SUBST1(X,Y,X7))=SUBST1(SUBST1(X,Y,X),Y,X7))∧
(∀X8 Y3.SUBST1(X,Y,SUBST1(X,Y,X8))=SUBST1(SUBST1(X,Y,X),Y,X8)∧
        SUBST1(X,Y,SUBST1(X,Y,Y3))=SUBST1(SUBST1(X,Y,X),Y,Y3)⊃
        SUBST1(X,Y,SUBST1(X,Y,X8).SUBST1(X,Y,Y3))=
        SUBST1(SUBST1(X,Y,X),Y,X8.Y3))⊃
(∀X9.SUBST1(X,Y,SUBST1(X,Y,X9))=SUBST1(SUBST1(X,Y,X),Y,X9))

66. 
;the term SUBST1(X,Y,X11.Y4) is replaced by:
;SUBST1(X,Y,X11).SUBST1(X,Y,Y4)
; failed to derive 
(∀X10.ATOM X10⊃SUBST1(X,Y,SUBST1(X,Y,X10))=SUBST1(SUBST1(X,Y,X),Y,X10))∧
(∀X11 Y4.SUBST1(X,Y,SUBST1(X,Y,X11))=SUBST1(SUBST1(X,Y,X),Y,X11)∧
         SUBST1(X,Y,SUBST1(X,Y,Y4))=SUBST1(SUBST1(X,Y,X),Y,Y4)⊃
         SUBST1(X,Y,SUBST1(X,Y,X11).SUBST1(X,Y,Y4))=
         SUBST1(SUBST1(X,Y,X),Y,X11.Y4))⊃
(∀X12.SUBST1(X,Y,SUBST1(X,Y,X12))=SUBST1(SUBST1(X,Y,X),Y,X12))
(∀X10.ATOM X10⊃SUBST1(X,Y,SUBST1(X,Y,X10))=SUBST1(SUBST1(X,Y,X),Y,X10))∧
(∀X11 Y4.SUBST1(X,Y,SUBST1(X,Y,X11))=SUBST1(SUBST1(X,Y,X),Y,X11)∧
         SUBST1(X,Y,SUBST1(X,Y,Y4))=SUBST1(SUBST1(X,Y,X),Y,Y4)⊃
         SUBST1(X,Y,SUBST1(X,Y,X11).SUBST1(X,Y,Y4))=
         SUBST1(SUBST1(X,Y,X),Y,X11.Y4))⊃
(∀X12.SUBST1(X,Y,SUBST1(X,Y,X12))=SUBST1(SUBST1(X,Y,X),Y,X12))

67. 
;file read in
;switched to LISPAX
;the proof LISPAX read in.
;you are now at the end of the proof lispax.
;EKL.INI read in
59. 
(decl subst (type: |ground⊗ground⊗ground→ground|) (syntype: constant))
(defax subst |∀x y z z1 z2.(atom z ⊃ subst(x,y,z) = if z = y then x else z)
∧ subst(x,y,z1.z2) = subst(x,y,z1).subst(x,y,z2)|)
(label substdef)

;you forgot this assumption:

(axiom |∀x y z.sexp subst(x,y,z)|)
(label simpinfo)

;then the obvious attempt works

(ue (phi |λz.subst(x,y,subst(x,y,z)) = subst(subst(x,y,x),y,z)|)
sexpinduction (open subst))
∀X7.SUBST(X,Y,SUBST(X,Y,X7))=SUBST(SUBST(X,Y,X),Y,X7)
 
;the problem with definitions seems to be caused by a bug:
;by teasing it a little bit, I got PDL-overflows out of it.
;I will look into it.
(ue (phi |λz.sexp subst(x,y,z)|) sexpinduction (open subst))
(label simpinfo)

Thanks and sorry for bothering you with something I might have figured
out for myself except that I'm in a bit of a hurry to understand it
ahead of my class.  We need more general ways of defining functions.
The first should, like Boyer and Moore, use a well-founded partial
ordering and a rank function.  This should be straightforward.  The
second is a definition principle that will allow defining functions
that don't necessarily terminate.  Carolyn knows how to do this without
the full apparatus of Scott orderings, continuity, etc.
(pretty-proof lispax lispax)

(decl flat (type: |ground⊗ground→ground|) (syntype: constant))
(defax flat |∀x y u.(atom x ⊃ flat(x,u) = x.u) ∧ flat(x.y,u) = flat(x,flat(y,u))|)
(label simpinfo)
(ue (phi |λx.∀u.listp flat(x,u)|) sexpinduction (open flat))
(label simpinfo)
(decl flatten (type: |ground→ground|) (syntype: constant))
(defax flatten |∀x y.(atom x ⊃ flatten(x) = list(x)) ∧ flatten(x.y) =
flatten(x) * flatten(y)|)
(label simpinfo)
(ue (phi |λx.listp flatten(x)|) sexpinduction (open flatten))
(label simpinfo)

(∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
      (∀U.FLAT(X,FLAT(Y,U))=FLAT(X,FLATTEN(Y))*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)

70. 
(ue (phi |λx.∀u.flat(x,u) = flatten(x)*u|) sexpinduction (open flat)
(open flatten) (use listdef mode: exact))
(trw |list(x)*u| (use listdef mode: exact))
(trw |∀x.(∀u.flat(x,u) = flatten(x)*u) ⊃ (∀u.flat(x,flat(y,u))=flat(x,flatten(y)

Hmm. A formula manipulator is different from a proof-checker.  The formula
manipulator never refuses to do a substitution because terms don't match.
It will compute in support of wrong reasoning just as cheerfully as in
support of correct reasoning.  I need a LISP and logic formula manipulator as
support for theorem proving.
60. 
61. ;Labeled.
61. ∀X U.LISTP FLAT(X,U)

62. ;Labeled.
62. 
63. 
64. ;Labeled.
64. ∀X.LISTP FLATTEN(X)

65. ;Labeled.
65.